/*    Copyright 2010 Tobias Marschall
 *
 *    This file is part of MoSDi.
 *
 *    MoSDi is free software: you can redistribute it and/or modify
 *    it under the terms of the GNU General Public License as published by
 *    the Free Software Foundation, either version 3 of the License, or
 *    (at your option) any later version.
 *
 *    MoSDi is distributed in the hope that it will be useful,
 *    but WITHOUT ANY WARRANTY; without even the implied warranty of
 *    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 *    GNU General Public License for more details.
 *
 *    You should have received a copy of the GNU General Public License
 *    along with MoSDi.  If not, see <http://www.gnu.org/licenses/>.
 */

package mosdi.fa;

import java.util.ArrayList;
import java.util.LinkedList;
import java.util.List;

import mosdi.util.BitArray;

public class AutomataUtils {

	/** For each state of the given automaton, the returned BitArray tells
	 *  whether it is reachable from the start state. */
	public static BitArray findReachableStates(CharacterAutomaton automaton) {
		BitArray reachableStates = new BitArray(automaton.getStateCount());
		reachableStates.set(automaton.getStartState(), true);
		LinkedList<Integer> toCheck = new LinkedList<Integer>();
		toCheck.add(automaton.getStartState());
		while (!toCheck.isEmpty()) {
			int state = toCheck.remove();
			for (int c=0; c<automaton.getAlphabetSize(); ++c) {
				int targetState = automaton.getTransitionTarget(state, c);
				if (!reachableStates.get(targetState)) {
					reachableStates.set(targetState, true);
					toCheck.add(targetState);
				}
			}
		}
		return reachableStates;
	}
	
	/** Computes a partition of all states into sets of equivalent states by using Hopcroft's
	 *  minimization algorithm. */
	public static Partition minimize(MinimizableAutomaton automaton) {
		int maxBlocks = automaton.getStateCount();
		int alphabetSize = automaton.getAlphabetSize();
		// step 1) construct inverse transition function
		InverseTransitionFunction inverse = new InverseTransitionFunction(automaton);
		// step 2) partition to start with is given by output table
		Partition partition = automaton.getStatePartition();
		// step 3) construct statesWithInverses[blockIdx][character]
		@SuppressWarnings("unchecked")
		List<Integer>[][] statesWithInverses = new List[maxBlocks][alphabetSize];
		for (int block : partition.blockIndices()) {
			for (int c=0; c<alphabetSize; ++c) {
				List<Integer> l = new ArrayList<Integer>();
				for (int state : partition.block(block)) {
					if (inverse.hasInverse(state, c)) l.add(state);
				}
				if (l.size()>0) statesWithInverses[block][c]=l;
			}
		}
		// step 4) create job list
		@SuppressWarnings("unchecked")
		LinkedList<Integer>[] toCheck = new LinkedList[alphabetSize];
		// BitArray to fastly determine if a block is in the list.
		BitArray[] toCheckBitArrays = new BitArray[alphabetSize];
		for (int c=0; c<alphabetSize; ++c) {
			toCheck[c]=new LinkedList<Integer>();
			toCheckBitArrays[c]=new BitArray(maxBlocks);
			for (int block : partition.blockIndices()) {
				if (statesWithInverses[block][c]==null) continue;
				toCheck[c].add(block);
				toCheckBitArrays[c].set(block, true);
			}
		}
//		for (int c=0; c<alphabetSize; ++c) {
//			// find largest set
//			int max = Integer.MIN_VALUE;
//			int maxIndex = -1;
//			for (int block : partition.blockIndices()) {
//				if (statesWithInverses[block][c]==null) continue;
//				if (statesWithInverses[block][c].size()>max) {
//					max=statesWithInverses[block][c].size();
//					maxIndex=block;
//				}
//			}
//			// now populate toCheck
//			toCheck[c]=new LinkedList<Integer>();
//			toCheckBitArrays[c]=new BitArray(maxBlocks);
//			for (int block : partition.blockIndices()) {
//				if (block==maxIndex) continue;
//				if (statesWithInverses[block][c]==null) continue;
//				toCheck[c].add(block);
//				toCheckBitArrays[c].set(block, true);
//			}
//			// TODO: this can lead to empty lists, is that correct? maybe do this: 
//			if (toCheck[c].isEmpty() && (maxIndex>=0)) {
//				toCheck[c].add(maxIndex);
//				toCheckBitArrays[c].set(maxIndex, true);
//			}
//		}
		// step 5) main iteration
		int character = 0;
		@SuppressWarnings("unchecked")
		LinkedList<Integer>[] statesToSplitOff = new LinkedList[maxBlocks];
		while (true) {
			int block=-1;
			for (int i=0; i<alphabetSize; ++i) {
				if (toCheck[character].size()>0) {
					block=toCheck[character].remove();
					toCheckBitArrays[character].set(block, false);
					break;
				}
				character=(character+1)%alphabetSize;
			}
			if (block==-1) break;
			// check which states have to be split off their blocks
			if (statesWithInverses[block][character]==null) continue;
			LinkedList<Integer> blocksToSplit = new LinkedList<Integer>();
			for (int stateWithInverse : statesWithInverses[block][character]) {
				for (int stateToBeSplitOff : inverse.get(stateWithInverse, character)) {
					int blockToSplit = partition.getBlockIndex(stateToBeSplitOff);
					if (statesToSplitOff[blockToSplit]==null) {
						blocksToSplit.add(blockToSplit);
						statesToSplitOff[blockToSplit]=new LinkedList<Integer>();
					}
					statesToSplitOff[blockToSplit].add(stateToBeSplitOff);
				}
			}
			// perform the split
			for (int blockToSplit : blocksToSplit) {
				// dont split if whole block is to be split off (which wouldnt be a split at all)
				if (statesToSplitOff[blockToSplit].size()==partition.blockSize(blockToSplit)) {
					// TODO: add something here?
					statesToSplitOff[blockToSplit]=null;
					continue;
				}
				// perform the split
				int newBlock = partition.splitOff(statesToSplitOff[blockToSplit]);
				// recalculate statesWithInverse for the two modified blocks
				int[] changedBlocks = {blockToSplit, newBlock};
				for (int i : changedBlocks) {
					for (int c=0; c<alphabetSize; ++c) {
						List<Integer> l = new ArrayList<Integer>();
						for (int state : partition.block(i)) {
							if (inverse.hasInverse(state, c)) l.add(state);
						}
						if (l.size()>0) statesWithInverses[i][c]=l;
						else statesWithInverses[i][c]=null;
					}
				}
				// update toCheck
				for (int c=0; c<alphabetSize; ++c) {
// conservative variant:
//					toCheck[c].add(newBlock);
//					toCheckBitArrays[c].set(newBlock, true);
//					if (!toCheckBitArrays[c].get(blockToSplit)) {
//						toCheck[c].add(blockToSplit);
//						toCheckBitArrays[c].set(blockToSplit, true);						
//					}
					if (toCheckBitArrays[c].get(blockToSplit)) {
						toCheck[c].add(newBlock);
						toCheckBitArrays[c].set(newBlock, true);
					} else {
						int i1 = statesWithInverses[blockToSplit][c]==null?0:statesWithInverses[blockToSplit][c].size();
						int i2 = statesWithInverses[newBlock][c]==null?0:statesWithInverses[newBlock][c].size();
						if (i1<=i2) {
							toCheck[c].add(blockToSplit);
							toCheckBitArrays[c].set(blockToSplit, true);							
						} else {
							toCheck[c].add(newBlock);
							toCheckBitArrays[c].set(newBlock, true);							
						}
					}
				}
				statesToSplitOff[blockToSplit]=null;
			}
		}
		partition.renumberBlocks();
		return partition;
	}
	
}
